Iof proof for Lemma gen hyp tp:
1. A : Type
2. e : A
3. H : A
Type
4. z : H(e)
5. A
Type
6. e
A
7.
x:A. (e = x) Type
z 
0
by (\p.
let i = get_int_arg `i` p
in let x = get_term_arg `x` p
inin let e = get_term_arg `e` p
in let A = get_term_arg `A` p
in
inAssertAtHyp
inAi
inA(
imk_exists_term (dv x) A (mk_equal_term A e x))
imkp)
i1: .....assertion..... NILNIL
i1: 
x:A. (e = x)
i2:
i2: 4. x:A. (e = x)
i2: 5. z : H(e)
i2: 6. A Type
i2: 7. e A
i2: 8. x:A. (e = x) Type
i2: z 0
i.